package interfaces.managers;
import interfaces.IIncidencia;
import interfaces.IRespuesta;
import interfaces.ITecnico;
import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;

public interface ICreadorRespuestasIncidenciasWithModel extends ICreadorRespuestasIncidencias, ICreadorRespuestasIncidenciasModel{
	@Pre ({"i != null && r != null && t != null #NullPointerException", "existeTecnico(t) && existeIncidencia(i) && !existeRespuesta(r) && i.getEsAbierta()"})
	@Pos ({"result == existeRespuesta(r) && existeTecnico(t) && existeIncidencia(i) && !i.getEsAbierta()"})
	public boolean creaRespuestaIncidencia(IIncidencia i, IRespuesta r, ITecnico t);
}
